\begin{tabbing}
$\forall$$A$, $B$:Type.
\\[0ex]strong{-}subtype($A$;$B$)
\\[0ex]$\Rightarrow$ (\=$\forall$$P$:($A$$\rightarrow$Prop), $Q$:($B$$\rightarrow$Prop).\+
\\[0ex]($\forall$$x$:$A$. $P$($x$) $\Rightarrow$ $Q$($x$)) $\Rightarrow$ strong{-}subtype(\{$x$:$A$$\mid$ $P$($x$) \};\{$x$:$B$$\mid$ $Q$($x$) \}))
\-
\end{tabbing}